/*
 * FormulaData.cuh
 *
 *  Created on: Sep 2, 2013
 *      Author: jaime
 */

#ifndef FORMULADATA_CUH_
#define FORMULADATA_CUH_

#include "../Utils/CUDAClauseVec.cuh"
#include <vector>
#include "../SATSolver/SolverTypes.cuh"
#include "../SATSolver/Configs.cuh"
#include <assert.h>

using namespace std;

class FormulaData {

private:
	CUDAClauseVec formula_dev;
	vector< Clause > formula_host;
	vector < Lit > set_literals;
	int number_of_clauses;
	int number_of_variables;
	int clauses_capacity;
	Var most_common_variable;
	int frequency_of_most_common_variable;
	int largest_clause_size;
	sat_status status_after_preprocessing;
	bool remove_unary;

public:
	FormulaData(int max_number_of_clauses, bool remove_unary);
	void add_clause(Lit* literals, int clause_size);
	void set_number_of_variables(int n_of_variables);
	void set_most_common_variable(Var variable, int frequency);

	CUDAClauseVec get_formula_dev();
	vector< Clause > * get_formula_host();
	int get_number_of_clauses();
	int get_number_of_variables();
	Var get_most_common_variable();
	int get_frequency_of_most_common_variable();
	int get_largest_clause_size();
	/**
	 * Copies the clauses that are on the host to the device.
	 * *** Make sure they have not been copied yet, otherwise they will be copied a second time.
	 */
	void copy_host_clauses_to_dev();
	vector< Lit > * get_set_literals();
	sat_status get_status_after_preprocessing();

	__host__ void print_fomula();
};

#endif /* FORMULADATA_CUH_ */
